『Introduction to Univalent Foundations of Mathematics with Agda』
https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html
1. どんなもの？
Agda
を使った
Univalent Foundations
の入門ページ
2. 先行研究と比べてどこがすごい？
3. 技術や手法のキモはどこ？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
#文献